perm filename APPL[EKL,SYS] blob
sn#864130 filedate 1988-08-04 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00011 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 representations of functions: two approaches
C00003 00003 first approach: functions as association lists
C00006 00004 facts about alists
C00009 00005 second approach: functions as lists of numbers
C00011 00006 PROOFS
C00012 00007 alist induction
C00014 00008 proof of facts about alists
C00018 00009 apparently stronger definition of samemap
C00020 00010 extensionality: better proof
C00023 00011 applfact has been proved already for nth
C00024 ENDMK
C⊗;
;representations of functions: two approaches
(wipe-out)
(get-proofs nth prf ekl sys)
;first approach: functions as association lists
(proof appalist)
(decl dom (syntype: constant) (type: |GROUND→GROUND|))
(defax dom |∀xa y alist.dom nil=nil∧
dom((xa.y).alist)=xa.dom alist| )
(label domdef)
(decl range (syntype: constant) (type: |GROUND→GROUND|))
(defax range |∀xa y alist.range nil=nil∧
range((xa.y).alist)=y.range alist| )
(label rangedef)
(decl functp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define functp |∀alist.functp(alist)≡uniqueness dom(alist)|)
(label functdef)
(decl injectp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define injectp |∀alist.injectp(alist)≡functp(alist)∧uniqueness range(alist)|)
(label injectdef)
(decl (appalist) (syntype: constant) (type: |ground⊗ground→ground|))
(define appalist |∀alist y.appalist(y,alist)=cdr assoc(y,alist)|)
(label appalistdef)
(decl (samemap) (syntype: constant) (type: |ground⊗ground→truthval|))
(define samemap
|∀alist alist1.samemap(alist,alist1)≡
mklset dom(alist)=mklset dom(alist1)∧
(∀y.yεmklset dom(alist)⊃appalist(y,alist)=appalist(y,alist1))|)
(label samemapdef)
(decl permutp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define permutp |∀alist.permutp(alist)≡
functp(alist)∧mklset(dom(alist))=mklset(range(alist))|)
(label permutp_def)
(axiom |∀chi.chi(nil)∧(∀xa y alist.chi(alist)⊃chi((xa.y).alist))⊃(∀alist.chi(alist))|)
(label alistinduction)
;facts about alists
(proof alistfacts)
(axiom |∀alist.listp(dom alist)|)
(label domsort)(label simpinfo)
(axiom |∀alist.listp(range alist)|)
(label rangesort)(label simpinfo)
(axiom |∀alist.length (dom(alist))=length alist|)
(label domlength)
(axiom |∀alist.length(dom(alist))=length(range(alist))|)
(label domrangelength)
(axiom |∀alist y.sexp appalist(y,alist)|)
(label appalistsort)(label simpinfo)
(axiom |∀alist y.¬yεmklset(dom(alist))⊃appalist(y,alist)=nil|)
(label trivial_appalist)
;Exercise:
;∀alist z.member(z,range alist)⊃(∃x.member(x.z,alist))
;(label member_range)
;∀alist x z.member(x.z,alist)⊃member(z,range(alist))
;(label membership_alist_range)
;∀alist x z.x=appalist(z,alist)∧atom assoc(z,alist)⊃null x
;(label trivial_assoc)
(axiom |∀alist.samemap(alist,alist)|)
(label samemap_equivalence)
(axiom |∀alist alist1.samemap(alist,alist1)⊃samemap(alist1,alist)|)
(label samemap_equivalence)
(axiom
|∀alist alist1 alist2.
samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|)
(label samemap_equivalence)
(axiom |∀alist1 alist2.samemap(alist1,alist2)≡
(mklset(dom(alist1))=mklset(dom(alist2))∧
(∀x.appalist(x,alist1)=appalist(x,alist2)))|)
(label samemap_def1)
;second approach: functions as lists of numbers
(proof appl)
(decl appl (syntype: constant) (type: |ground⊗ground→ground|))
(define appl |∀u i.appl(u,i)=nth(u,i)|)
(label appldef)
;extensionality for functions
(axiom |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v|)
(label extensionality)
(axiom |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)|)
(label applfacts) (label simpinfo)
;predicates for functions
(decl (into) (syntype: constant) (type: |ground→truthval|))
(define into |∀u.into(u)=(∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length u)|)
(label intodef)
(decl (onto) (syntype: constant) (type: |ground→truthval|))
(define onto |∀u.onto(u)=(into(u)∧(∀n.n<length u⊃member(n,u)))|)
(label ontodef)
(decl (perm) (syntype: constant) (type: |ground→truthval|))
(define perm |∀u.perm(u)=onto(u)|)
;injectivity is given by the predicate inj
(save-proofs appl)
;PROOFS
;alist induction
(wipe-out)
(get-proofs appl prf ekl sys)
(proof alistind)
1. (assume |chi nil|)
(label alind0)
2. (assume |∀xa y alist.chi(alist)⊃chi((xa.y).alist)|)
(label alind1)
3. (assume |alistp u⊃chi u|)
(label alind2)
4. (assume |alistp (x.u)|)
(label alind3)
5. (ue (u |x.u|) alistdef1 *)
;¬ATOM X∧ATOM CAR X∧ALISTP U
6. (ue ((xa.|car x|)(y.|cdr(x)|)(alist.u)) alind1 * alind3 alind2)
;CHI(X.U)
;deps: (ALIND1 ALIND2 ALIND3)
7. (ci alind3)
;ALISTP X.U⊃CHI(X.U)
;deps: (ALIND1 ALIND2)
8. (ci alind2)
;(ALISTP U⊃CHI(U))⊃(ALISTP X.U⊃CHI(X.U))
;deps: (ALIND1)
9. (ue (phi |λu.alistp(u)⊃chi(u)|) listinduction * alind0 alind1)
;∀U.ALISTP U⊃CHI(U)
10. (derive |∀alist.chi alist| *)
;deps: (ALIND0 ALIND1)
11. (ci (alind0 alind1))
;CHI(NIL)∧(∀XA Y ALIST.CHI(ALIST)⊃CHI((XA.Y).ALIST))⊃(∀ALIST.CHI(ALIST))
;proof of facts about alists
(wipe-out)
(get-proofs appl prf ekl sys)
(proof alistproofs)
(unlabel simpinfo domsort rangesort appalistsort)
;domsort
1. (ue (chi |λalist.listp dom(alist)|) alistinduction (open dom))
;∀ALIST.LISTP DOM(ALIST)
(label simpinfo domsort)
;rangesort
2. (ue (chi |λalist.listp range(alist)|) alistinduction (open range))
;∀ALIST.LISTP RANGE(ALIST)
(label simpinfo rangesort)
;domlength
3. (ue (chi |λalist.length dom alist=length alist|) alistinduction (open dom))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH ALIST
;domrangelength
4. (ue (chi |λalist.length(dom alist)=length(range alist)|) alistinduction
(open dom range))
;∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))
;appalistsort
5. (ue (chi |λalist.sexp appalist(y,alist)|) alistinduction
(part 1(open appalist assoc)))
;∀ALIST.SEXP APPALIST(Y,ALIST)
(label simpinfo appalistsort)
;trivial appalist
6. (ue (chi |λalist.¬(yεmklset dom(alist))⊃appalist(y,alist)=nil|) alistinduction
(part 1 (open epsilon mklset dom appalist assoc member)))
;∀ALIST.¬YεMKLSET(DOM(ALIST))⊃APPALIST(Y,ALIST)=NIL
;member range
7. (ue (chi |λalist.member(z,range alist)⊃(∃x.member(x.z,alist))|)
alistinduction
(open range member)(use normal mode: always))
;∀ALIST.MEMBER(Z,RANGE(ALIST))⊃(∃X.MEMBER(X.Z,ALIST))
;membership alist range
8. (trw |∀x y.x=y⊃cdr x=cdr y|)
;∀X Y.X=Y⊃CDR X=CDR Y
9. (ue ((x.|x.z|)(y.|xa.y|)) *)
;X.Z=XA.Y⊃Z=Y
10. (ue (chi |λalist.member(x.z,alist)⊃member(z,range alist)|)
alistinduction
(open appalist assoc range member)
(use demorgan1 * normal mode: always))
;∀ALIST.MEMBER(X.Z,ALIST)⊃MEMBER(Z,RANGE(ALIST))
;trivial assoc
;(ue (chi |λalist.x=cdr assoc(z,alist)∧atom assoc(z,alist)⊃null x|)
; alistinduction
; (open assoc))
;∀ALIST.X=CDR ASSOC(Z,ALIST)∧ATOM ASSOC(Z,ALIST)⊃NULL X
;samemap
(proof samemap)
1. (trw |samemap(alist,alist)|(open samemap))
;SAMEMAP(ALIST,ALIST)
2. (trw |samemap(alist,alist1)⊃samemap(alist1,alist)| (open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)⊃SAMEMAP(ALIST1,ALIST)
3. (trw |samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|
(open samemap mklset dom))
;SAMEMAP(ALIST,ALIST1)∧SAMEMAP(ALIST1,ALIST2)⊃SAMEMAP(ALIST,ALIST2)
;apparently stronger definition of samemap
(wipe-out)
(get-proofs appl prf ekl sys)
(proof samemapdef)
1. (assume |samemap(alist1,alist2)|)
2. (rw * (open samemap))
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))
3. (trw |¬yεmklset(dom(alist1))⊃appalist(y,alist1)=appalist(y,alist2)|
(use trivial_appalist mode: always)
(use * mode: exact))
;¬YεMKLSET(DOM(ALIST1))⊃APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2)
4. (ue ((q.|yεmklset dom(alist1)|)(p.|appalist(y,alist1)=appalist(y,alist2)|))
excluded_middle * -2)
;APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2)
5. (derive |mklset(dom(alist1))=mklset(dom(alist2))∧
∀y.appalist(y,alist1)=appalist(y,alist2)| (-3 *))
6. (ci -5)
;SAMEMAP(ALIST1,ALIST2)⊃
;MKLSET(DOM(ALIST1))=MKLSET(DOM(ALIST2))∧
;(∀Y.APPALIST(Y,ALIST1)=APPALIST(Y,ALIST2))
7. (derive |samemap(alist1,alist2)≡
(mklset(dom(alist1))=mklset(dom(alist2))∧
(∀x.appalist(x,alist1)=appalist(x,alist2)))| *)
;extensionality: better proof
(wipe-out)
(get-proofs appl prf ekl sys)
(proof extensionality)
(show doubleinduction)
;labels: DOUBLEINDUCTION
; (AXIOM
; |∀PHI2.(∀U V X Y.PHI2(NIL,U)∧PHI2(U,NIL)∧(PHI2(U,V)⊃PHI2(X.U,Y.V)))⊃
; (∀U V.PHI2(U,V))|)
;first attempt:
;(ue (phi2 |λu v.length u=length v∧(∀i.i<length u⊃nth(u,i)=nth(v,i))⊃u=v|)
; doubleinduction (open nth))
;(∀U V X Y.(LENGTH U=LENGTH V∧(∀I.I<LENGTH V⊃NTH(U,I)=NTH(V,I))⊃U=V)⊃
; (LENGTH U=LENGTH V∧(∀I.I<LENGTH V'⊃NTH(X.U,I)=NTH(Y.V,I))⊃X.U=Y.V))⊃
;(∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH V⊃NTH(U,I)=NTH(V,I))⊃U=V)
1. (assume |LENGTH U=LENGTH V∧(∀I.I<LENGTH V⊃NTH(U,I)=NTH(V,I))⊃U=V|)
(label ext1)
2. (assume |LENGTH U=LENGTH V|)
(label ext2)
3. (assume |∀I.I<LENGTH V'⊃NTH(X.U,I)=NTH(Y.V,I)|)
(label ext3)
4. (ue (i 0) * ext2)
;X=Y
(label ext4)
;deps: (EXT2 EXT3)
5. (ue (i |i'|) ext3 ext2)
;I<LENGTH V⊃NTH(U,I)=NTH(V,I)
(label ext5)
;deps: (EXT2 EXT3)
6. (derive |u=v| (ext1 ext2 ext5))
(label ext6)
;deps: (EXT1 EXT2 EXT3)
7. (trw |x.u=y.v| (use ext4 ext6 mode: exact))
;X.U=Y.V
;deps: (EXT1 EXT2 EXT3)
8. (ci (ext2 ext3))
;LENGTH U=LENGTH V∧(∀I.I<LENGTH U'⊃NTH(X.U,I)=NTH(Y.V,I))⊃X.U=Y.V
;deps: (EXT1)
9. (ci ext1)
;(LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃NTH(U,I)=NTH(V,I))⊃U=V)⊃
;(LENGTH U=LENGTH V∧(∀I.I<LENGTH U'⊃NTH(X.U,I)=NTH(Y.V,I))⊃X.U=Y.V)
10. (ue (phi2 |λu v.length u=length v∧(∀i.i<length u⊃nth(u,i)=nth(v,i))⊃u=v|)
doubleinduction (open nth) *)
;∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH V⊃NTH(U,I)=NTH(V,I))⊃U=V
;applfact has been proved already for nth
11. (trw |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)|
(open appl) nthmember)
;∀U I.I<LENGTH U⊃SEXP APPL(U,I)∧MEMBER(APPL(U,I),U)